\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Cmd}$:Type, ${\it Master}$:AbsInterface(chain\_master()),\+
\\[0ex]${\it Config}$:AbsInterface(chain\_config()), ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)),
\\[0ex]$m$:(\{$e$:E(${\it Master}$)$\mid$ $\uparrow$cmseq?(${\it Master}$($e$))\} $\rightarrow$E(${\it Config}$)).
\-\\[0ex]master{-}antecedent\{i:l\}(${\it es}$;${\it Cmd}$;${\it Master}$;${\it Config}$;${\it Sys}$;$m$) $\in$ $\mathbb{P}$
\end{tabbing}